翻訳と辞書 Words near each other ・ Markov chains on a measurable state space ・ Markov decision process ・ Markov information source ・ Markov kernel ・ Markov logic network ・ Markov model ・ Markov number ・ Markov partition ・ Markov perfect equilibrium ・ Markov process ・ Markov Processes International ・ Markov property ・ Markov random field ・ Markov renewal process ・ Markov reward model ・ Markov Reward Model Checker ・ Markov spectrum ・ Markov strategy ・ Markov switching multifractal ・ Markov tree ・ Markov's inequality ・ Markov's principle ・ Markova Crkva ・ Markova Sušica ・ Markovac ・ Markovac (Mladenovac) ・ Markovac (Velika Plana) ・ Markovac (Vršac) ・ Markovac Križevački ・ Markovac Našički Dictionary Lists mini英和辞書 mini和英辞書 Webster 1913 Latin-English FOLDOC Wikipedia English ウィキペディア

翻訳と辞書　辞書検索 [ 開発暫定版 ] スポンサード リンク Markov Reward Model Checker ： ウィキペディア英語版 Markov Reward Model Checker The Markov Reward Model Checker (MRMC)() is a model checker for discrete-time and continuous-time Markov reward models. It supports reward extensions of PCTL and (CSL ) ((PRCTL ) and (CSRL )), and allows for the automated verification of properties concerning long-run and instantaneous rewards as well as cumulative rewards. In particular, it supports to check the reachability of a set of goal states (by only visiting legal states before) under a time and an accumulated reward constraint. MRMC has been developed by the (Formal Methods & Tools (FMT) group ) at the University of Twente, The Netherlands and the (Software Modeling and Verification (MOVES) group ) at RWTH Aachen University, Germany under the guidance of Prof. Dr. Ir. Joost-Pieter Katoen. An example snapshot of the tool usage is provided on the right. == MRMC details == MRMC is a command-line tool written in the C programming language and based on a sparse matrix representation. This allows MRMC to be small and fast. The empirical study of MRMC performance in comparison to other model checkers such as (PRISM ), (ETMCC ), (Vesta ), and (Ymer ) is available (here ). MRMC is supplied for Linux, Mac OS X and Microsoft Windows (compilable under Cygwin) platforms. The tool is distributed under the GNU General Public License (GPL). MRMC expects five input files: # .tra-file describing the probability or rate matrix, # .ctmdpi-file describing the rate matrix and indicating the transition-labeling, # .lab-file indicating the state-labeling with atomic propositions, # .rew-file specifying the state reward structure, # .rewi-file specifying the impulse reward structure. which have a simple text format. For (CSL ) and PCTL verification, the latter two files may be omitted. Additionally when working with MDPs, the .tra-file is substituted by the .ctmdpi-file. The properties of interest, specified in PCTL, (CSL ), (PRCTL ) or (CSRL ) are accepted through the command-prompt interface of the tool. A sketch of the tool architecture is provided on the right. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Markov Reward Model Checker」の詳細全文を読む スポンサード リンク 翻訳と辞書 : 翻訳のためのインターネットリソース Copyright(C) kotoba.ne.jp 1997-2016. All Rights Reserved.